﻿<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8" /><meta http-equiv="Content-Style-Type" content="text/css" /><meta name="generator" content="Aspose.Words for .NET 15.1.0.0" /><title></title></head><body><div><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:24pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:24pt">二元决策图基础</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">译自：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">An Introduction to Binary Decision Diagrams</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">作者：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">Henrik Reif Andersen</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.001.png" width="302" height="426" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">Efficient Algorithms and Programs, Fall 1999</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">课程笔记</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">电子邮件</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">: hra@itu.dk. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">网址</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">: </span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">http://www.itu.dk/people/hra</span></p><p style="margin:0pt; text-align:center"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">哥本哈根信息技术大学</span></p><p style="margin:0pt; page-break-before:always"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">前言</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">本讲义是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">二元决策图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Binary Decision Diagrams</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的简单介绍，包含一些背景知识和核心算法。更多的细节可以从</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Bryant</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">最初的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">无冗降序二元决策图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> Reduced Ordered Binary Decision Diagrams</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）论文</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[Bry86]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以及总览论文</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[Bry92]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中找到。最新的扩展称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">布尔表达式图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> Boolean Expression Diagrams</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">），可以在</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[AH97]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中找到。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">本讲义是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">fall 1996</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（基于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1995</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1994</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的基础版本）的修正版。主要的变更如下：第一，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">现在被看作全局图（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">global graph</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）中的节点，它有固定的变量顺序，且代表了高效</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">包的最高水平。第二，增加了</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">正准性引理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">canonicity lemma</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的证明。第三，重构了讲述算法的章节。第四，改进了项目方案。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">致谢</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">感谢</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">fall 1994</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1995</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1996</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中的学生协助我调试和改进这份讲义。谢谢</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> Hans Rischel, Morten Ulrik Sørensen, Niels Maretti, Jørgen Staunstrup, Kim Skak Larsen, Henrik Hulgaard, </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以及很多网上的朋友帮我改进并找出印刷错误。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">目录</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">布尔表达式</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">2. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">范式</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">3. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">二元决策图</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">构造、操作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.1 Mk</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.2 Build</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.3 Apply</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.4 Restrict</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.5 SatCount, AnySat AllSat</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.6 Simplify</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">4.7 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">存在量化和替换</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">5. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">实现</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的指令</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">实例：用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">解决问题</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6.1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">八皇后问题</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6.2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">组合电路的正确性</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6.3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">组合电路的等价性</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">7 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">使用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">验证</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">7.1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">骑士之旅</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">8 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">项目：一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">包</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Reference</span></p><p style="margin:0pt; page-break-before:always"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">1. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">布尔表达式</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">经典的对</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">真值</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">truth value</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的演算包括了：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">a. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">布尔变量</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">……</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">b. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">定值</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">true 1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">false 0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">c. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">操作符：合取</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∧</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，析取</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∨</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，非</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">¬</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，蕴涵</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇒</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，双条件</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。这三种符号组成了布尔表达式。布尔变量也可称作命题变量或者命题字幕。布尔表达式也被称作命题逻辑。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">布尔表达式用以下规则形式化定义：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t ::= x | 0 | 1 | ¬t  |  t </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∧ t | t  ∨</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> t | t  ⇒ t | t  ⇔ t,</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">其中，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表了布尔变量的集合。这称作布尔表达式的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">抽象语法</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">abstract syntax</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。为了解决结合的混淆，具体的语法包含了括号。并且根据传统习惯，所有的操作符都被赋予了优先级。优先级即：按以下顺序优先结合：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">¬</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∧</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∨</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇒</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。例如：</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.002.png" width="298" height="22" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">布尔函数中的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">……</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表了这个变量的取值是由真值表决定的，见</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">真值指派</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">truth assignment</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）按照顺序把值赋予变量，即：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">4</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">意指将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">赋予</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1   </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">赋予</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">4</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。在这种情况下，上边的表达式的值为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, 0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">4</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">将使上边的表达式的值为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.003.png" width="521" height="131" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">真值的集合通常用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Β = {0, 1} </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示。如果我们将布尔表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的变量次序固定下来，那么我们可以将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">视为一个由</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">映射向</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的函数，其中</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表变量的个数。注意，顺序的选取对于定义该函数而言是非常关键的。思考例子</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇒y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">：如果我们的选取的顺序使</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x&lt;y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，那么函数即为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f(x,y) =  x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇒y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，此情况下第一个参数蕴含了第二个参数使函数为真。如果我们的选取的顺序使</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x&gt;y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，那么函数即为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f(y,x) =  x⇒y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，此情况下第二个参数蕴含了第一个参数使函数为真。在接下来介绍的布尔表达式的简洁表示中，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">变量的顺序至关紧要</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">两个布尔表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic"> t' </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相等，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">当且仅当它</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">们在所有的真值指派下，都取相同的真值。当一个布尔表达式在所有的真值指派下都为真，那么它被称作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">重言式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">tautology</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，又叫永真式）。当一个布尔表达式至少在一种真值指派下为真，那么它被称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">可满足的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">satisfiable</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">.1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">¬</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∨</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示所有其他的逻辑操作符。以此证明所有的布尔表达式都可仅用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">¬</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∧</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∨</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和变量表达。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 1.2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">证明：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic"> t' </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相等当且仅当</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇒</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic"> t' </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为重言式。是否可证当</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">  ¬</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为重言式时，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为可满足的。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">2. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">范式</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果一个布尔表达式只由变量的合取和变量的否定的析取组成，那么它为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">析取范式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Disjunctive Normal Form)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。即，如果它由如下形式构成</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.004.png" width="665" height="56" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">且每一个</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.005.png" width="11" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都是变量</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.006.png" width="13" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">或者其否定形式</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.007.png" width="25" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。例如下面是一个非常有名的函数（异或）：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.008.png" width="180" height="38" alt="" style="-aw-left-pos:0.91pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:9.84pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(1)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">更简明的表示为：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.009.png" width="93" height="71" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:2.44pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相同的，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">合取范式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Conjunctive Normal Form)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">可写作：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.010.png" width="94" height="71" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:3.66pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">其中</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.005.png" width="11" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">均为变量或者变量的否定。则不难推出命题：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">命题</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">任何布尔表达式都可以表示为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">或者</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">一般地，一个布尔表达式是否是可满足的很难识别。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Cook</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">对此有一个著名的定理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[Coo71]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">定理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Cook</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">）</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">布尔表达式的可满足性为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-complete</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（对于不熟悉</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-completeness</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">概念的读者，可以看下面的总结：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-complete</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的问题可以用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">指数时间</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">exponential time</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的算法解决。没有已知的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">多项式时间</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">polynomial </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">time</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的算法可以解决任意一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-complete</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的问题，而且也很难证明有这样的多项式时间的算法存在。虽然如此，也没有人可以证明这样的算法不存在。）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Cook</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">定理甚至对</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">也有效。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">可满足性问题可由多项式时间的算法计算，但是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的恒真检查是很难的（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">co-NP complete</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。尽管可满足性之于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，恒真检查之于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都是容易的，这对我们帮助不大：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的转换是指数时间的，以下例子可以说明这个问题。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">考虑由变量</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.011.png" width="94" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">构成的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF:</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.012.png" width="253" height="29" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:4.26pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相应的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是一个从</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">000…000</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">至</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">111…111</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">位二进制数的析取，其中第</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">i</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">位代表了选取</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.013.png" width="16" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">还是</span><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.014.png" width="16" height="26" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:inline" /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">:</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.015.png" width="256" height="128" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:4.9pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">当原表达式的大小与</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">成正比时，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">则与</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">成正比。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">下一节介绍了比</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">更可取的范式。特别是对于可满足性问题和恒真问题有极其有效的算法。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2.1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">描述一个判断</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DNF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是否为可满足的多项式时间算法。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2.2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">描述一个判断</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">CFN</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是否为恒真的多项式时间算法。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2.3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">证明命题</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2.4</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">解释</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Cook</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">定理是如何证明判断两个布尔表达式是否不等价是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-hard</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2.5</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">解释为什么给出一个检查两个布尔表达式等价性的算法</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，则恒真和可满足性是可判断的。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">3. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:16pt; font-weight:bold">二分决策图</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">让形如</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">,y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">称作一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">if-then-else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">操作符</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，其定义为：</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.016.png" width="308" height="49" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:4.26pt; -aw-wrap-type:topbottom" /><br /><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">这样对于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t→t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">,t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，当</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">、</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为真，或者</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为假，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为真时，该表达式为真。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">被称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">测试表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">test expression</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。所有的操作符都可以仅用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">if-then-else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">操作符以及</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">、</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示。这可由将所有的测试由（非否定形式的）变量和没有在其他地方出现的变量的方式达成。这样就构成了一种新的范式。例如，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">¬x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">即是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(x→0,1)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">即是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x→(y→1,0),(y→</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0,1)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。因为所有的变量都要出现在测试表达式里，所以</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">应表示为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> x→1,0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><table cellspacing="0" cellpadding="0" style="border-collapse:collapse; margin-left:0pt; width:499.35pt"><tr><td style="border-bottom-color:#000000; border-bottom-style:solid; border-bottom-width:0.75pt; border-left-color:#000000; border-left-style:solid; border-left-width:0.75pt; border-right-color:#000000; border-right-style:solid; border-right-width:0.75pt; border-top-color:#000000; border-top-style:solid; border-top-width:0.75pt; padding:2.38pt; vertical-align:top; width:493.1pt"><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">IF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">判断范式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">If-then-else Normal Form, INF)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是一个完全只由</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">if-then-else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">操作符和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">、</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">构成的布尔表达式，其中的测试只在变量上进行。</span></p></td></tr></table><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果我们用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> t[0/x]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表将布尔表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中的所有变量</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">取代，那么易得：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.017.png" width="665" height="45" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">这被称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">关于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">香农扩展</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Shannon Expansion</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。这一个简单的等式有很多有用的应用。第一个应用是从任何表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中生成</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">不包含任何变量，那么</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">要么是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，要么是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，这两种形式都是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。否则我们可以生成</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">关于任一</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的香农扩展。这样无论</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t[0/x]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">还是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t[1/x]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都比</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">少一个变量。我们可以递归地从这两者中找到</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">；称他们</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。这样一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x→t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">,t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">已证明：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">命题</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">任何布尔表达式都与一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">形式的表达式等价。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">例</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">考虑布尔表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t = (x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。如果我们可以找到一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，且指定变量的顺</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">序：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，通过香农扩展，我们可以获得以下表达式：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.018.png" width="225" height="271" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:6.09pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">将此表达式展示为一个书。这样的树也被称为决策树。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">许多表达式可以轻易地证明完全相同，所以找出它们是一件很诱人的工作。例如，我们可以用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">000</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">110</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">001</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">111</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，如果我们用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">000</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">取代</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">11</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">右边的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">110</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，同样地用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">001</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">取代</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">11</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">右边的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">111</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，可以发现</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">00</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">11</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是完全相同的。所以可以在</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">00</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">取代</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">11</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果我们可以找出所有相等的子表达式，并把它们全都简化，我们即可获得一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">二元决策图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">binary decision diagram</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。它不再是一个布尔表达式构成的树，而是一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">有向无环图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">directed acyclic graph</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">DAG</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.019.png" width="665" height="434" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">由共享子树出发，我们可以将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">写成：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.020.png" width="228" height="190" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0.6pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">每一个子表达式都可视作图的一个节点。这样一个节点要么是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">或</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">汇聚节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，要么就是有后继的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">分支节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。（译者注，为了与《计算机程序设计艺术（第四卷）》一书统一，本文的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">terminal</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">译为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">汇聚节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">sink node</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">；</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">non-terminal</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">译为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">分支节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">branch </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">node</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。然而，《计算机程序设计艺术（第四卷）》中还有根节点的概念。本文并未突出根节点有何特殊性，所以可以一概而论。）分支节点有一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">低分支</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">low-edge</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">LO</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">），相关于表达式的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">部分；和一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">高分支</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">high-edge</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">HI</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">），代表了</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">then</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">部分，如</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。注意，节点的数目，从决策树中的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">9</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，降低到了</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。不难想象，如果分支节点是一个其他巨大的决策树，那么就会节省非常客观的数目。因为在递归构建</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">INF</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中，我们以约定的顺序选取了变量，变量以同样的顺序出现在了从根节点出发的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中。所</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">展示的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">也是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.021.png" width="665" height="360" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 4</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">展示了四个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。一些测试（例如图</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）是冗余的，因为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">HI</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">LO</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都指向了相同的节点。这样的不必要的测试可以移除：所有这样冗余的节点，都将直接指向其子节点的线段代替。如果所有的相同节点都是共享的，所有的冗余测试都将被移除，那么这个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">则称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">已约化的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">reduced</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。这样的一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">即为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">有非常多有用的性质。这些性质的核心是下面的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">正准性引理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">canonicity lemma</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。（大部分情况下使用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">这个词，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都是在讨论</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.022.png" width="665" height="398" alt="" style="-aw-left-pos:56.69pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:4.14pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以上内容总结如下：</span></p><table cellspacing="0" cellpadding="0" style="border-collapse:collapse; margin-left:0pt; width:499.35pt"><tr><td style="border-bottom-color:#000000; border-bottom-style:solid; border-bottom-width:0.75pt; border-left-color:#000000; border-left-style:solid; border-left-width:0.75pt; border-right-color:#000000; border-right-style:solid; border-right-width:0.75pt; border-top-color:#000000; border-top-style:solid; border-top-width:0.75pt; padding:2.38pt; vertical-align:top; width:493.1pt"><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是一个有根节点的，有向无环图，且有：</span></p><p style="margin:0pt 0pt 0pt 36pt; text-indent:-18pt"><span style="font-family:OpenSymbol; font-size:12pt">•</span><span style="font:7.0pt 'Times New Roman'">&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0; </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">至</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">出度</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">out-degree</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）的汇聚节点，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">或</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，且有</span></p><p style="margin:0pt 0pt 0pt 36pt; text-indent:-18pt"><span style="font-family:OpenSymbol; font-size:12pt">•</span><span style="font:7.0pt 'Times New Roman'">&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0; </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">一个出度为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的分支节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的集合。两个向外的边分别由</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">low(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">high(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">给出。（在图中，分别由虚线和实线表式。）一个变量</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">var(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相关于此节点。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是有序的，当且仅当图中所有的路径经过的变量都遵循一个给定的线性序</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt;...&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">　</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(O)BDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是已约化的，当且仅当：</span></p><p style="margin:0pt 0pt 0pt 36pt; text-indent:-18pt"><span style="font-family:OpenSymbol; font-size:12pt">•</span><span style="font:7.0pt 'Times New Roman'">&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0; </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">唯一性</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">uniqueness</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）没有两个相同的节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">绑定了相同的变量，且有相同的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">LO</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">HI</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">后继，即：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">var(u) = var(v), low(u) = low(v), high(u) = high(v)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">可得</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u = v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，且</span></p><p style="margin:0pt 0pt 0pt 36pt; text-indent:-18pt"><span style="font-family:OpenSymbol; font-size:12pt">•</span><span style="font:7.0pt 'Times New Roman'">&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0;&#xa0; </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">无冗余测试</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">non-redundant tests</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）没有任何一个节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">有相同的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">LO</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">HI</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">后继，即：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">low(u) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">≠ </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">high(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p></td></tr></table><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 5</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">展示了有序性和已约化性。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.023.png" width="665" height="184" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">有很多有趣的性质。它们提供了一个简洁的布尔表达式的表示方式，并且所有的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的逻辑操作都有快速算法。这些都基于这样一个事实：对于每一个函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt"> : </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，有且仅有一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">与之对应。这意味着，有且仅有一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代表恒真和恒假：汇聚节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。因此，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">检验一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">是否恒真或恒假（可能）有常数时间的方法。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（对于布尔表达式，这个问题是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">NP-complete</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的。）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为了更详细的解释，我们必须说明用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示函数的意义。第一，很容易发现</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的节点是如何归纳地定义布尔表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的：汇聚节点表示布尔常数（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">标示的分支节点是一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">if-then-else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表达式，其测试条件为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，其两个分支为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">LO</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">HI</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">给出的布尔表达式。形式化定义如下：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= 0</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = 1</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = var(u) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→ t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">high(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">low(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为布尔变量节点。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; … &lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的变量顺序，我们将每一个节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">相关于函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, …, b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∈</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">映射至</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">t</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, …, b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的真值。我们可以得到关键的引理：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">引理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">正准性引理，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">C</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">anonicity lemma</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">对于任意函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">f : </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，有且仅有一个变量顺序为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; … &lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，如</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = f(</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">证明：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">证明过程为对</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">参数数量的归纳：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(1) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">对于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n=0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，有且仅有两个布尔函数：恒真函数，恒假函数。因为任何</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都有至少一个分支节点是非常量。因此这两个函数都分别对应一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">：汇聚节点：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(2)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">假设：已证引理</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">在</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个参数下成立。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">那么在</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n+1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个参数时，使</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f : B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n+1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→ </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为任意</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n+1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个参数的布尔函数。定义两个函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个参数的函数，其由函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">把第一个参数分别改为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">或</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">得出：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">( x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">) = f(b,  x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> b </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">∈</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> B</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（有时</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">称为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">关于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">负协函子</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">negative co-factor)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">、</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">正协函子</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">positive co-factor</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">））这两个函数构成了如下等式：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">( x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">),  f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">( x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">) </span><span style="width:12.37pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(3)</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:14pt">因为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">都只需要</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个参数，根据假设，有唯一的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">构成</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">这有两种情况：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(2.1) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，那么</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，且</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">=  f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。因此</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">即为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。根据变量顺序，这也是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的唯一</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">已经存在于以</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为根节点的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">应该为根节点。然而，如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，那么</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">] = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">low(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">且</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">] = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">high(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。因为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">=f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">=  f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，左右分支是相同的，这与</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">无冗余测试</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">性质相悖。（此情况为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的取值对于函数取值没有影响。这说明该函数对应的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">就是省略掉</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">之后的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">参数的函数</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，译者注）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(2.2) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">如果</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">≠</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，那么可以从归纳假设中得到</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">≠</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（使用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n+1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">代替</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">, … , x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）。使</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">var(u) = x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">low(u) = u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">high(u) = u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的节点。也就是</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">→</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">,f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，它是已约化的。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">通过假设</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= </span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">且</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">  f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，根据式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(3)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，可以推断出</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。假设</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是一个其他的节点且</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，很明显，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">一定依赖于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，也就是说</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">] </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">≠</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">] </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（否则</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[0/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">] = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[1/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">]  = f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，与假设矛盾）。因为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">有序性</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，这意味着</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">var(v) = x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = var(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。而且，从</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = f </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">可以得出，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">low(v)  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= </span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u0 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">且</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">high(v)  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= </span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1  </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">= f</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">u1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，根据假设</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">low(v) = u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> = low(u) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">high(v) = u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> =high(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。根据</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">已约化</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">性质，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u = v</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">重要的结论如下：汇聚节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是对于任何变量顺序，唯一为恒真的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。判断</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">是不是汇聚节点</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">可用常数时间的操作判断。这对恒假同样成立。实际上，判断两个布尔函数是否相同，可以通过在同一个图中构造它们的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，然后检查他们</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的节点是否相同。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的变量顺序对于其大小的影响非常大。考虑表达式：</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">然后以</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt;</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的顺序构造</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 6</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">），那么将有</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">9</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个节点。</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Figure 3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">中的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">只有</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个节点。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><img src="89d3dd5b-7ec3-4ff3-8336-5b5eb11beb14.024.png" width="665" height="476" alt="" style="-aw-left-pos:0pt; -aw-rel-hpos:column; -aw-rel-vpos:paragraph; -aw-top-pos:0pt; -aw-wrap-type:topbottom" /><br /></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 3.1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">if-then-else</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">操作和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">、</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示所有的操作符。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 3.2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以顺序</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt;</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt;</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">画</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 3.3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt;</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&lt; y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的顺序画</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∨(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。它们与</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> Fiugre 3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> Figure 6 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">有何不同？根据这些例子，什么顺序可以为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)∧…∧(x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">⇔y</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">3</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">) </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">生成较小的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">？</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 3.4 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">举例一系列的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0 ≤ n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">），它们使决策树指数式增长。也就是说，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:sub">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的大小为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">θ(n)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的话，其决策树为</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">θ(2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; vertical-align:super">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">练习</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">3.5</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">6</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个变量构造最大的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">（</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">41</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">个节点？</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> 1+2+4+6+16+8+2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">构造、操作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">ROBDD</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">在上一节，我们了解了如何通过一个简单的递归过程使用布尔表达式构造</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。现在考虑如何构造无冗的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。一个简单的方式是先构造</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，再进行简化。另外一个有效的方法为，在构造中简化</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">OBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。下面将作详细解释。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">为了描述这个过程，我们需要指出一种</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的表示方式。节点由数字</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0, </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1, 2, ...</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">表示，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">0</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">保留为汇聚节点。</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.1 Mk</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.2 Build</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.3 Apply</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.4 Restrict</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.5 SatCount, AnySat AllSat</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.6 Simplify</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">4.7 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">存在量化和替换</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">5. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">实现</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">的指令</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">6. </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">实例：用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">解决问题</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">6.1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">八皇后问题</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">6.2 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">组合电路的正确性</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">6.3 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">组合电路的等价性</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">7 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">使用</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">验证</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">7.1 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">骑士之旅</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">8 </span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">项目：一个</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">包</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">本项目将实现一个包含</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">操作的简易包。整个包应</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">该包含以下操作：</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Init(n)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">初始化包。使用从</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">到</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">n</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">个变量。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Print(u)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">在标准输出中打印</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。这对</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">Debug</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">非常有用。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Mk(i,l,h)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">返回一个节点的编号</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，其中</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">var(u)  =i</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">low(u) = l</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">high(u) = h</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。这个可能是一个已有的节点，或者一个新建的节点。这个操作要注意不要违反了</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">的约化性。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Build(t)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">从一个布尔表达式中建立</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。你可以专注于表达式</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">¬x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，或者它们的合取。（为什么？）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Apply(op,u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:bold; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">,u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:bold; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">构造将</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">op</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">应用于</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:normal; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:normal; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">ROBDD</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Restrict(u,j,b)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">通过真值指派</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">[b/x</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:normal; vertical-align:sub">j</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">]</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，限定</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">ROBDD u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">SatCount(u)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">返回集合</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">sat(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">中的元素数量。（用一个可以包含非常大的数的类型，如浮点数。）</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">AnySat(u)</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">返回一个符合要求的</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">的真值指派。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">子项目</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 1</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">实现第四节中的表</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">T</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">H</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">以及它们的操作。在这之上，实现操作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Init(n)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Print(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Mk(i,l,h)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">子项目</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 2</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">继续添加操作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">Build(t)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">和</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">Apply(op,u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:normal; vertical-align:sub">1</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">,u</span><span style="font-family:'LM Roman Unslanted 10'; font-size:8pt; font-weight:normal; vertical-align:sub">2</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">子项目</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold"> 3</span></p><p style="margin:0pt"><span style="width:22.15pt; text-indent:0pt; display:inline-block"></span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">添加操作</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">Restrict(u,j,b)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">SatCount(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">，</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">AnySat(u)</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:normal">。</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">Reference</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:18pt; font-weight:bold">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[AH97]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Andersen, Henrik Reif, and Henrik Hulgaard. "Boolean expression diagrams."</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:italic">Logic in Computer Science, 1997. LICS'97. Proceedings., 12th Annual IEEE Symposium on</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">. IEEE, 1997.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="http://www.sciencedirect.com/science/article/pii/S0890540101929487/pdf?md5=aa1c74f8d5af7f06b028376d6c6af645&amp;pid=1-s2.0-S0890540101929487-main.pdf"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">http://www.sciencedirect.com/science/article/pii/S0890540101929487/pdf?md5=aa1c74f8d5af7f06b</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">028376d6c6af645&amp;pid=1-s2.0-S0890540101929487-main.pdf</span></a></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[Bry86]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Bryant RE. Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on. 1986 Aug;100(8):677-91.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="https://pdfs.semanticscholar.org/f5c1/b943517eabf5ef33d95d922f1343e88960d0.pdf"><span style="font-family:'Arial, sans-serif'; font-size:11.5pt">https://pdfs.semanticscholar.org/f5c1/b943517eabf5ef33d95d922f1343e88960d0.pdf</span></a></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[Bry92]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Bryant RE. Symbolic Boolean manipulation with ordered binary-decision </span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">diagrams. ACM Computing Surveys (CSUR). 1992 Sep 1;24(3):293-318.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="https://www.di.ens.fr/~jv/HomePage/dea/bryantonBDD.pdf"><span style="font-family:'Arial, sans-serif'; font-size:11.5pt">http://www.di.ens.fr/~jv/HomePage/dea/bryantonBDD.pdf</span></a></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[CBM89]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Coudert O, Berthet C, Madre JC. Verification o</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">f synchronous sequential machines based on symbolic execution. InInternational Conference on Computer Aided Verification 1989 Jun 12 (pp. 365-373). Springer, Berlin, Heidelberg.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="https://link.springer.com/chapter/10.1007/3-540-52148-8_30"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">https://link.springer.com/chapter/10.1007/3-540-52148-8_30</span></a></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[CLR90]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Cormen TH. Introduction to algorithms. MIT press; 2009 Jul 31.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="http://ressources.unisciel.fr/.../%5BCormen-AL2011%5DIntroduction_To_Algorithms-A3.pdf"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">http://</span></a><a style="color:#000000" href="http://ressources.unisciel.fr/.../%5BCormen-AL2011%5DIntroduction_To_Algorithms-A3.pdf"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">ressources.unisciel.fr/.../%5BCormen-AL2011%5DIntroduction_To_Algorithms-A3.pdf</span></a></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">[Co</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">o71]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Cook SA. The complexity of theorem-proving procedures. InProceedings of the third annual ACM symposium on Theory of computing 1971 May 3 (pp. 151-158). ACM.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="line-height:12.65pt; margin:0pt 0pt 14.15pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:normal; font-weight:bold">Link: </span><a style="color:#000000" href="https://www.cs.toronto.edu/~sacook/homepage/1971.pdf"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-style:normal">https://www.cs.toronto.edu/~sacook/homepage/1971.pdf</span></a></p><p style="line-height:12.65pt; margin:0pt 2.35pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">[</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Mil89]</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">Milner R. Communication and concurrency. New York etc.: Prentice hall; 1989 Jan 3.</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">&#xa0;</span></p><p style="margin:0pt"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt; font-weight:bold">Link:</span><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt"> </span><a style="color:#000000" href="https://www.goodreads.com/book/show/788766.Communication_and_Concurrency"><span style="font-family:'LM Roman Unslanted 10'; font-size:12pt">https://www.goodreads.com/book/show/788766.Communication_and_Concurrency</span></a></p></div><div class="cnzz" style="display: none;">
	        <script src="http://s95.cnzz.com/stat.php?id=1253551100&web_id=1253551100" language="JavaScript"></script>
            </div>
            <div class="docpe" style="position: absolute;color: white;margin-left:-450;">
            <a target="_blank" href="http://www.docpe.com">档铺网——在线文档免费处理</a>
            </div>
            </body></html>
